Inference at * 1 
Iof proof for Lemma do-apply-mu':



1. A : Type
2. P : A
3. d : x:A. Dec(n:. ((P(x,n))))
4. x : A
  (isl((TERMOF{p-mu-decider:ObjectId, 1:l, i:l}(A,P,d,x)).1))
   {((P(x,outl((TERMOF{p-mu-decider:ObjectId, 1:l, i:l}(A,P,d,x)).1))))
   & (i:{0..outl((TERMOF{p-mu-decider:ObjectId, 1:l, i:l}(A,P,d,x)).1)}. ((P(x,i))))} 

latex

 by (GenConclAtAddr [1;1;1;1]) 
CollapseTHEN ((Thin (-1)) 
CollapseTHEN (((D (-1)) 

CoCollapseTHEN (Reduce 0)) 
CollapseTHEN (((D (-2)) 
CollapseTHEN (Reduce 0)) 
CollapseTHEN (
C(RepUR ``p-mu`` ( -1)) 
CollapseTHEN ((MaAuto) 
CollapseTHEN ((Unfold `guard` ( 0)) 

CoCollapseTHEN (MaAuto))))))) 

latex

C.

Definitions	s = t, p-mu-decider, , , f(a), x:A. B(x), left + right, , A  B, Void, True, if b then t else f fi , , {x:A| B(x)} , A c B, p-mu(P;x), P  Q, {T}, P & Q, x:A  B(x), {i..j}, Top, x:A.B(x), Dec(P), A, b, x:AB(x), Type, x:A. B(x), t  T, False
Lemmas	p-mu-decider, bool wf, decidable wf, assert wf, nat wf, top wf, p-mu wf, true wf, false wf